(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 6))
(let ((e4 3))
(let ((e5 0))
(let ((e6 (/ e5 (- e3))))
(let ((e7 (+ e6 v1)))
(let ((e8 (* e7 e7)))
(let ((e9 (- e7 e8)))
(let ((e10 (* e8 e9)))
(let ((e11 (+ e7 v0)))
(let ((e12 (+ v2 v1)))
(let ((e13 (* v1 e11)))
(let ((e14 (* (- e3) e9)))
(let ((e15 (* e12 e7)))
(let ((e16 (+ e12 v1)))
(let ((e17 (* e7 (- e5))))
(let ((e18 (- v1)))
(let ((e19 (* e4 e15)))
(let ((e20 (>= e17 e10)))
(let ((e21 (> e19 v1)))
(let ((e22 (>= v2 e9)))
(let ((e23 (<= e15 e16)))
(let ((e24 (>= e13 v2)))
(let ((e25 (> e10 e9)))
(let ((e26 (= e7 e7)))
(let ((e27 (> e19 e12)))
(let ((e28 (> e15 e11)))
(let ((e29 (>= e8 v1)))
(let ((e30 (< e14 e9)))
(let ((e31 (< e11 e6)))
(let ((e32 (> e14 e9)))
(let ((e33 (> e16 e8)))
(let ((e34 (= e16 v2)))
(let ((e35 (<= e17 e9)))
(let ((e36 (= v1 e10)))
(let ((e37 (= e6 e18)))
(let ((e38 (> v1 e18)))
(let ((e39 (distinct e11 e12)))
(let ((e40 (> e16 e7)))
(let ((e41 (distinct e12 e14)))
(let ((e42 (< e13 e11)))
(let ((e43 (<= e14 e8)))
(let ((e44 (< e19 e17)))
(let ((e45 (distinct e8 e7)))
(let ((e46 (= e10 e13)))
(let ((e47 (>= v0 e17)))
(let ((e48 (= e9 v2)))
(let ((e49 (distinct v1 e19)))
(let ((e50 (distinct e10 e12)))
(let ((e51 (= e17 e12)))
(let ((e52 (= e8 e13)))
(let ((e53 (>= e10 e16)))
(let ((e54 (= e16 e11)))
(let ((e55 (> e16 e10)))
(let ((e56 (= e9 e10)))
(let ((e57 (= e11 v2)))
(let ((e58 (<= e14 e15)))
(let ((e59 (< v2 v0)))
(let ((e60 (<= e11 e11)))
(let ((e61 (<= e17 e19)))
(let ((e62 (distinct e14 e13)))
(let ((e63 (>= e16 e14)))
(let ((e64 (>= e16 e6)))
(let ((e65 (distinct e12 e13)))
(let ((e66 (>= e10 e7)))
(let ((e67 (distinct e9 e11)))
(let ((e68 (= e14 v0)))
(let ((e69 (<= e12 e19)))
(let ((e70 (< e12 e9)))
(let ((e71 (distinct v0 e11)))
(let ((e72 (> e15 e18)))
(let ((e73 (not e48)))
(let ((e74 (not e63)))
(let ((e75 (ite e54 e34 e54)))
(let ((e76 (=> e41 e21)))
(let ((e77 (or e55 e23)))
(let ((e78 (or e77 e43)))
(let ((e79 (= e56 e35)))
(let ((e80 (= e78 e73)))
(let ((e81 (= e66 e30)))
(let ((e82 (=> e26 e47)))
(let ((e83 (or e44 e80)))
(let ((e84 (xor e24 e64)))
(let ((e85 (= e39 e58)))
(let ((e86 (=> e68 e59)))
(let ((e87 (not e22)))
(let ((e88 (or e71 e69)))
(let ((e89 (xor e72 e86)))
(let ((e90 (= e57 e83)))
(let ((e91 (xor e46 e33)))
(let ((e92 (and e60 e87)))
(let ((e93 (and e91 e28)))
(let ((e94 (not e76)))
(let ((e95 (and e84 e32)))
(let ((e96 (xor e90 e75)))
(let ((e97 (not e42)))
(let ((e98 (or e45 e93)))
(let ((e99 (= e65 e67)))
(let ((e100 (xor e99 e79)))
(let ((e101 (or e51 e50)))
(let ((e102 (or e27 e31)))
(let ((e103 (or e37 e25)))
(let ((e104 (= e97 e82)))
(let ((e105 (=> e40 e74)))
(let ((e106 (and e62 e52)))
(let ((e107 (=> e101 e94)))
(let ((e108 (xor e106 e85)))
(let ((e109 (not e89)))
(let ((e110 (xor e38 e104)))
(let ((e111 (or e96 e49)))
(let ((e112 (not e105)))
(let ((e113 (xor e112 e29)))
(let ((e114 (not e61)))
(let ((e115 (and e102 e20)))
(let ((e116 (= e103 e36)))
(let ((e117 (ite e116 e53 e107)))
(let ((e118 (=> e108 e81)))
(let ((e119 (xor e115 e88)))
(let ((e120 (or e100 e111)))
(let ((e121 (and e114 e98)))
(let ((e122 (or e120 e109)))
(let ((e123 (or e119 e119)))
(let ((e124 (not e70)))
(let ((e125 (or e113 e92)))
(let ((e126 (not e123)))
(let ((e127 (= e125 e124)))
(let ((e128 (ite e95 e95 e95)))
(let ((e129 (= e127 e118)))
(let ((e130 (or e128 e117)))
(let ((e131 (xor e130 e121)))
(let ((e132 (xor e129 e122)))
(let ((e133 (ite e126 e110 e126)))
(let ((e134 (or e133 e133)))
(let ((e135 (= e134 e131)))
(let ((e136 (xor e132 e135)))
e136
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
